H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 0.47100000000000003 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/Monad.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ LR

mainModule Monad

((liftM5 :: (c -> d -> a -> b -> e -> f) -> Maybe c -> Maybe d -> Maybe a -> Maybe b -> Maybe e -> Maybe f) :: (c -> d -> a -> b -> e -> f) -> Maybe c -> Maybe d -> Maybe a -> Maybe b -> Maybe e -> Maybe f)

module Monad where

import qualified Maybe
import qualified Prelude

liftM5 :: Monad d => (e -> a -> c -> f -> b -> g) -> d e -> d a -> d c -> d f -> d b -> d g

liftM5

f m1 m2 m3 m4 m5

m1 >>= (\x1 ->m2 >>= (\x2 ->m3 >>= (\x3 ->m4 >>= (\x4 ->m5 >>= (\x5 ->return (f x1 x2 x3 x4 x5))))))

module Maybe where

import qualified Monad
import qualified Prelude

Lambda Reductions:
The following Lambda expression

\x5→return (f x1 x2 x3 x4 x5)

is transformed to

liftM50 f x1 x2 x3 x4 x5 = return (f x1 x2 x3 x4 x5)

The following Lambda expression

\x4→m5 >>= liftM50 f x1 x2 x3 x4

is transformed to

liftM51 m5 f x1 x2 x3 x4 = m5 >>= liftM50 f x1 x2 x3 x4

The following Lambda expression

\x3→m4 >>= liftM51 m5 f x1 x2 x3

is transformed to

liftM52 m4 m5 f x1 x2 x3 = m4 >>= liftM51 m5 f x1 x2 x3

The following Lambda expression

\x2→m3 >>= liftM52 m4 m5 f x1 x2

is transformed to

liftM53 m3 m4 m5 f x1 x2 = m3 >>= liftM52 m4 m5 f x1 x2

The following Lambda expression

\x1→m2 >>= liftM53 m3 m4 m5 f x1

is transformed to

liftM54 m2 m3 m4 m5 f x1 = m2 >>= liftM53 m3 m4 m5 f x1

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

mainModule Monad

((liftM5 :: (f -> c -> a -> b -> d -> e) -> Maybe f -> Maybe c -> Maybe a -> Maybe b -> Maybe d -> Maybe e) :: (f -> c -> a -> b -> d -> e) -> Maybe f -> Maybe c -> Maybe a -> Maybe b -> Maybe d -> Maybe e)

module Maybe where

import qualified Monad
import qualified Prelude

module Monad where

import qualified Maybe
import qualified Prelude

liftM5 :: Monad a => (e -> f -> g -> d -> b -> c) -> a e -> a f -> a g -> a d -> a b -> a c

liftM5

f m1 m2 m3 m4 m5

m1 >>= liftM54 m2 m3 m4 m5 f

liftM50

f x1 x2 x3 x4 x5

return (f x1 x2 x3 x4 x5)

liftM51

m5 f x1 x2 x3 x4

m5 >>= liftM50 f x1 x2 x3 x4

liftM52

m4 m5 f x1 x2 x3

m4 >>= liftM51 m5 f x1 x2 x3

liftM53

m3 m4 m5 f x1 x2

m3 >>= liftM52 m4 m5 f x1 x2

liftM54

m2 m3 m4 m5 f x1

m2 >>= liftM53 m3 m4 m5 f x1

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule Monad

((liftM5 :: (a -> f -> b -> e -> c -> d) -> Maybe a -> Maybe f -> Maybe b -> Maybe e -> Maybe c -> Maybe d) :: (a -> f -> b -> e -> c -> d) -> Maybe a -> Maybe f -> Maybe b -> Maybe e -> Maybe c -> Maybe d)

module Monad where

import qualified Maybe
import qualified Prelude

liftM5 :: Monad c => (e -> a -> g -> f -> d -> b) -> c e -> c a -> c g -> c f -> c d -> c b

liftM5

f m1 m2 m3 m4 m5

m1 >>= liftM54 m2 m3 m4 m5 f

liftM50

f x1 x2 x3 x4 x5

return (f x1 x2 x3 x4 x5)

liftM51

m5 f x1 x2 x3 x4

m5 >>= liftM50 f x1 x2 x3 x4

liftM52

m4 m5 f x1 x2 x3

m4 >>= liftM51 m5 f x1 x2 x3

liftM53

m3 m4 m5 f x1 x2

m3 >>= liftM52 m4 m5 f x1 x2

liftM54

m2 m3 m4 m5 f x1

m2 >>= liftM53 m3 m4 m5 f x1

module Maybe where

import qualified Monad
import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

mainModule Monad

(liftM5 :: (d -> c -> e -> a -> b -> f) -> Maybe d -> Maybe c -> Maybe e -> Maybe a -> Maybe b -> Maybe f)

module Maybe where

import qualified Monad
import qualified Prelude

module Monad where

import qualified Maybe
import qualified Prelude

liftM5 :: Monad e => (f -> b -> c -> g -> a -> d) -> e f -> e b -> e c -> e g -> e a -> e d

liftM5

f m1 m2 m3 m4 m5

m1 >>= liftM54 m2 m3 m4 m5 f

liftM50

f x1 x2 x3 x4 x5

return (f x1 x2 x3 x4 x5)

liftM51

m5 f x1 x2 x3 x4

m5 >>= liftM50 f x1 x2 x3 x4

liftM52

m4 m5 f x1 x2 x3

m4 >>= liftM51 m5 f x1 x2 x3

liftM53

m3 m4 m5 f x1 x2

m3 >>= liftM52 m4 m5 f x1 x2

liftM54

m2 m3 m4 m5 f x1

m2 >>= liftM53 m3 m4 m5 f x1

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="liftM5",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="liftM5 vy3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="liftM5 vy3 vy4",fontsize=16,color="grey",shape="box"];4 -> 5[label="",style="dashed", color="grey", weight=3];
5[label="liftM5 vy3 vy4 vy5",fontsize=16,color="grey",shape="box"];5 -> 6[label="",style="dashed", color="grey", weight=3];
6[label="liftM5 vy3 vy4 vy5 vy6",fontsize=16,color="grey",shape="box"];6 -> 7[label="",style="dashed", color="grey", weight=3];
7[label="liftM5 vy3 vy4 vy5 vy6 vy7",fontsize=16,color="grey",shape="box"];7 -> 8[label="",style="dashed", color="grey", weight=3];
8[label="liftM5 vy3 vy4 vy5 vy6 vy7 vy8",fontsize=16,color="black",shape="triangle"];8 -> 9[label="",style="solid", color="black", weight=3];
9[label="vy4 >>= liftM54 vy5 vy6 vy7 vy8 vy3",fontsize=16,color="burlywood",shape="box"];42[label="vy4/Nothing",fontsize=10,color="white",style="solid",shape="box"];9 -> 42[label="",style="solid", color="burlywood", weight=9];
42 -> 10[label="",style="solid", color="burlywood", weight=3];
43[label="vy4/Just vy40",fontsize=10,color="white",style="solid",shape="box"];9 -> 43[label="",style="solid", color="burlywood", weight=9];
43 -> 11[label="",style="solid", color="burlywood", weight=3];
10[label="Nothing >>= liftM54 vy5 vy6 vy7 vy8 vy3",fontsize=16,color="black",shape="box"];10 -> 12[label="",style="solid", color="black", weight=3];
11[label="Just vy40 >>= liftM54 vy5 vy6 vy7 vy8 vy3",fontsize=16,color="black",shape="box"];11 -> 13[label="",style="solid", color="black", weight=3];
12[label="Nothing",fontsize=16,color="green",shape="box"];13[label="liftM54 vy5 vy6 vy7 vy8 vy3 vy40",fontsize=16,color="black",shape="box"];13 -> 14[label="",style="solid", color="black", weight=3];
14[label="vy5 >>= liftM53 vy6 vy7 vy8 vy3 vy40",fontsize=16,color="burlywood",shape="box"];44[label="vy5/Nothing",fontsize=10,color="white",style="solid",shape="box"];14 -> 44[label="",style="solid", color="burlywood", weight=9];
44 -> 15[label="",style="solid", color="burlywood", weight=3];
45[label="vy5/Just vy50",fontsize=10,color="white",style="solid",shape="box"];14 -> 45[label="",style="solid", color="burlywood", weight=9];
45 -> 16[label="",style="solid", color="burlywood", weight=3];
15[label="Nothing >>= liftM53 vy6 vy7 vy8 vy3 vy40",fontsize=16,color="black",shape="box"];15 -> 17[label="",style="solid", color="black", weight=3];
16[label="Just vy50 >>= liftM53 vy6 vy7 vy8 vy3 vy40",fontsize=16,color="black",shape="box"];16 -> 18[label="",style="solid", color="black", weight=3];
17[label="Nothing",fontsize=16,color="green",shape="box"];18[label="liftM53 vy6 vy7 vy8 vy3 vy40 vy50",fontsize=16,color="black",shape="box"];18 -> 19[label="",style="solid", color="black", weight=3];
19[label="vy6 >>= liftM52 vy7 vy8 vy3 vy40 vy50",fontsize=16,color="burlywood",shape="box"];46[label="vy6/Nothing",fontsize=10,color="white",style="solid",shape="box"];19 -> 46[label="",style="solid", color="burlywood", weight=9];
46 -> 20[label="",style="solid", color="burlywood", weight=3];
47[label="vy6/Just vy60",fontsize=10,color="white",style="solid",shape="box"];19 -> 47[label="",style="solid", color="burlywood", weight=9];
47 -> 21[label="",style="solid", color="burlywood", weight=3];
20[label="Nothing >>= liftM52 vy7 vy8 vy3 vy40 vy50",fontsize=16,color="black",shape="box"];20 -> 22[label="",style="solid", color="black", weight=3];
21[label="Just vy60 >>= liftM52 vy7 vy8 vy3 vy40 vy50",fontsize=16,color="black",shape="box"];21 -> 23[label="",style="solid", color="black", weight=3];
22[label="Nothing",fontsize=16,color="green",shape="box"];23[label="liftM52 vy7 vy8 vy3 vy40 vy50 vy60",fontsize=16,color="black",shape="box"];23 -> 24[label="",style="solid", color="black", weight=3];
24[label="vy7 >>= liftM51 vy8 vy3 vy40 vy50 vy60",fontsize=16,color="burlywood",shape="box"];48[label="vy7/Nothing",fontsize=10,color="white",style="solid",shape="box"];24 -> 48[label="",style="solid", color="burlywood", weight=9];
48 -> 25[label="",style="solid", color="burlywood", weight=3];
49[label="vy7/Just vy70",fontsize=10,color="white",style="solid",shape="box"];24 -> 49[label="",style="solid", color="burlywood", weight=9];
49 -> 26[label="",style="solid", color="burlywood", weight=3];
25[label="Nothing >>= liftM51 vy8 vy3 vy40 vy50 vy60",fontsize=16,color="black",shape="box"];25 -> 27[label="",style="solid", color="black", weight=3];
26[label="Just vy70 >>= liftM51 vy8 vy3 vy40 vy50 vy60",fontsize=16,color="black",shape="box"];26 -> 28[label="",style="solid", color="black", weight=3];
27[label="Nothing",fontsize=16,color="green",shape="box"];28[label="liftM51 vy8 vy3 vy40 vy50 vy60 vy70",fontsize=16,color="black",shape="box"];28 -> 29[label="",style="solid", color="black", weight=3];
29[label="vy8 >>= liftM50 vy3 vy40 vy50 vy60 vy70",fontsize=16,color="burlywood",shape="box"];50[label="vy8/Nothing",fontsize=10,color="white",style="solid",shape="box"];29 -> 50[label="",style="solid", color="burlywood", weight=9];
50 -> 30[label="",style="solid", color="burlywood", weight=3];
51[label="vy8/Just vy80",fontsize=10,color="white",style="solid",shape="box"];29 -> 51[label="",style="solid", color="burlywood", weight=9];
51 -> 31[label="",style="solid", color="burlywood", weight=3];
30[label="Nothing >>= liftM50 vy3 vy40 vy50 vy60 vy70",fontsize=16,color="black",shape="box"];30 -> 32[label="",style="solid", color="black", weight=3];
31[label="Just vy80 >>= liftM50 vy3 vy40 vy50 vy60 vy70",fontsize=16,color="black",shape="box"];31 -> 33[label="",style="solid", color="black", weight=3];
32[label="Nothing",fontsize=16,color="green",shape="box"];33[label="liftM50 vy3 vy40 vy50 vy60 vy70 vy80",fontsize=16,color="black",shape="box"];33 -> 34[label="",style="solid", color="black", weight=3];
34[label="return (vy3 vy40 vy50 vy60 vy70 vy80)",fontsize=16,color="black",shape="box"];34 -> 35[label="",style="solid", color="black", weight=3];
35[label="Just (vy3 vy40 vy50 vy60 vy70 vy80)",fontsize=16,color="green",shape="box"];35 -> 36[label="",style="dashed", color="green", weight=3];
36[label="vy3 vy40 vy50 vy60 vy70 vy80",fontsize=16,color="green",shape="box"];36 -> 37[label="",style="dashed", color="green", weight=3];
36 -> 38[label="",style="dashed", color="green", weight=3];
36 -> 39[label="",style="dashed", color="green", weight=3];
36 -> 40[label="",style="dashed", color="green", weight=3];
36 -> 41[label="",style="dashed", color="green", weight=3];
37[label="vy40",fontsize=16,color="green",shape="box"];38[label="vy50",fontsize=16,color="green",shape="box"];39[label="vy60",fontsize=16,color="green",shape="box"];40[label="vy70",fontsize=16,color="green",shape="box"];41[label="vy80",fontsize=16,color="green",shape="box"];}